w-discrete-constraint(w)
== i, x:Id.
== (discrete(i;x))
==  (constant_function(s(i;0).x;;w.T(i,x))
==  & (k:Knd, v:kindcase(k; a.w.TA(i,a); l,t.w.M(l,t) ), s:EState(w.T(i)).
==  & (constant_function(s(x);;w.T(i,x))
==  & ( constant_function(((w-machine(w;i).2).1)(k,v,s,x);;w.T(i,x)))) 

latex

---

clarification:

w-discrete-constraint(w)
== i:Id, x:Id.
== (w-discrete(w;i;x))
==  (constant_function(w-s(w; i; 0; x);;w.T(i,x))
==  & (k:Knd, v:kindcase(k; a.w.TA(i,a); l,t.w.M(l,t) ), s:EState(w.T(i)).
==  & (constant_function(s(x);;w.T(i,x))
==  & ( constant_function(((w-machine(w;i).2).1)(k,v,s,x);;w.T(i,x)))) 

latex

Definitions	Id, b, discrete(i;x), P & Q, s(i;t).x, #$n, Knd, kindcase(k; a.f(a); l,t.g(l;t) ), w.TA, w.M, x:A. B(x), EState(T), P  Q, constant_function(f;A;B), t.1, t.2, w-machine(w;i), , f(a), w.T
FDL editor aliases	w-discrete-constraint